$\forall$$b$:$\mathbb{B}$, $A$:Type, $p$, $q$:$A$. if $b$ then $p$ else $q$ fi  $\in$ $A$